\begin{tabbing}
$\forall$\=$M$:MsgA, $k$:Knd, $l$:IdLnk, $s$:$M$.state, $v$:$M$.V($k$), $i$:Id,\+
\\[0ex]${\it ms}$:(${\it tg}$:Id$\times$if source($l$) = $i$$\rightarrow$ $M$.da(rcv($l$,${\it tg}$)) else Top fi) List.
\-\\[0ex]$M$.send($k$;$l$;$s$;$v$;${\it ms}$;$i$) $\in$ Prop
\end{tabbing}